Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
length: empty set
nil: empty set
0: empty set
length1: empty set


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
length: empty set
nil: empty set
0: empty set
length1: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
length: empty set
nil: empty set
0: empty set
length1: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, FROM} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {length, length1, LENGTH1, LENGTH, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)


The hidden terms of R are:

from(s(X))

Every hiding context is built from:

s on positions {1}
from on positions {1}

Hence, the new unhiding pairs DPu are :

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(from(s(X))) → FROM(s(X))

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 1 less node.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
                ↳ QCSDPSubtermProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {length, length1, U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
                ↳ QCSDPSubtermProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {length, length1} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {length, length1, LENGTH, LENGTH1} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH1(X) → LENGTH(X)
LENGTH(cons(X, Y)) → LENGTH1(Y)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


The following rules are not useable and can be deleted:

from(x0) → cons(x0, from(s(x0)))
length(nil) → 0
length(cons(x0, x1)) → s(length1(x1))
length1(x0) → length(x0)


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSUsableRulesProof
                  ↳ QCSDP
                    ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {LENGTH, LENGTH1, length, length1} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH1(X) → LENGTH(X)
LENGTH(cons(X, Y)) → LENGTH1(Y)

R is empty.
The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


Using the order
Polynomial interpretation [25]:

POL(LENGTH(x1)) = 2·x1   
POL(LENGTH1(x1)) = 1 + 2·x1   
POL(cons(x1, x2)) = 2 + 2·x2   

the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

LENGTH1(X) → LENGTH(X)
LENGTH(cons(X, Y)) → LENGTH1(Y)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSUsableRulesProof
                  ↳ QCSDP
                    ↳ QCSDPReductionPairProof
                      ↳ QCSDP
                        ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {length, length1} are not replacing on any position.

The TRS P consists of the following rules:
none

R is empty.
The set Q consists of the following terms:

from(x0)
length(nil)
length(cons(x0, x1))
length1(x0)


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.